COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	!Axioms for proving existence of set of equivalence classes!
C00003 ENDMK
C⊗;
COMMENT !Axioms for proving existence of set of equivalence classes!

DECLARE PREDPAR R 2;

AXIOM EQUIV:	∀x.R(x,x)
		∀x y.(R(x,y) ≡ R(y,x))
		∀x y z.(R(x,y) ∧ R(y,z) ⊃ R(x,z));;

DECLARE INDVAR a;

DECLARE INDVAR r1 r2;

COMMENT !To show: ∃r.(∀x y.(xεa ∧ yεa ⊃ (R(x,y) ≡ ∃s.(sεr ∧ xεs ∧ yεs)))
∧ ∀s.(sεr ⊃ ∃x.(xεs ∧ ∀y.(R(x,y) ≡ yεs)))) !